Nuprl Lemma : es-first-implies 0,22

the_es:ES, je:E. first(j (e <loc j
latex


Definitionst  T, x:AB(x), P  Q, P & Q, P  Q, E, first(e), b, (e <loc e'), False, A, ES
Lemmasevent system wf, es-axioms, assert wf, es-first wf, es-E wf

origin